 Process
Analysis Toolkit (PAT) 3.5
Help |
A process is defined as an equation in
the following syntax, P(x1, x2,
..., xn) = Exp; where P
is the process name, x1, ..., xn is an
optional list of process parameters and Exp is a process expression. The
process expression determines the computational logic of the process. A process
without parameters is written either as P() or P. A defined process may be
referenced by its name (with the valuations of the parameters). Process
referencing allows a flexible form of recursion. The deadlock process is written as
follows, Stop The process does absolutely nothing.
The process which terminates immediately
is written as follows, Skip
The process terminates and then behaves
exactly the same as Stop. A simple event is a name for representing
an observation. Given a process P, the following describes a process
which performs e first and then behaves as specified by process
P. e
-> P where e
is an event. An event is the abstraction of an observation. Event prefixing
is a common construct for describing systems. The following describes a simple
vending machine which takes in a coin and dispatches a coffee every time.
VM() =
insertcoin -> coffee -> VM();
Where event
insertcoin models the event of inserting
a coin into the machine and event coffee models the event of getting
coffee out of the machine. An event may be in a compound form, e.g.,
x.exp1.exp2 where x is a name and exp1 and exp2
are expressions which are composed variables (e.g., process parameters,
channel input variables or global variables). For instance, Phil(i) = get.i.(i
+ 1)%N -> Rest(); where i is a parameter of the process. We remark
event expressions which contains global variables, though allowed, may result in
runtime exception if combined with alphabetized parallel composition. Refer to
parallel composition for
details. Note: event name is an
arbitrary string of form ('a'..'z'|'A'..'Z'|'_')
('a'..'z'|'A'..'Z'|'0'..'9'|'_')*. However, global variable names, global
constant names, process names, process parameter names, propositions names
can not be used as event name. One exception is the channel names are allowed,
because we may want to use channel name in a specific process to simulate the
channel behaviors and use refinement checking to compare with real channel
events. Statement
Block inside Events (aka
Data Operations) An event can be attached with assignments
which update global variables as in the following example, add{x = x+1;} ->
Stop; where x
is a global variable. In general, an event may be attached with
a statement block of a sequential program (which may contain local
variables, if-then-else, while, math
function etc.). This kind of event-prefix process is called data
operation in PAT. The exact syntax of the statements can be found in Grammar Rules. Notice that the sequential program is considered
as an atomic action. That is, no interleaving of other processes before the
sequential program finishes. In other words, once started, the sequential
program continues to execute until it finished without being interrupted. From
another point of view, the event can be viewed as a labeled piece of code.
The event name is used for constructing meaningful counterexamples (or
associating fairness with the code, as discussed below). For instance, the
following process can be used to find the maximum value of a given
array. Note: both global variable (e.g., array,
max) and local variables (e.g., index) are allowed to be
used and updated in the sequential program. While process arguments
and channel input variables can only be used without being
updated. The scope of the local variable is only inside the sequential
program and starts from the place of declaration. PAT does not
support process level local variables so that there is no need
to maintain a changing heap/stack to gain the efficiency.
Alternatively, process level local variables can be modeled using global
variables easily. Note: Data operation supports local variable array, assume
the following process is valid in PAT: event
{var array[5];} -> Process where local variable array's(here is the array) elements are
initialized to zero. Note: the semi-colon in the last expression in
the statement block is optional for the simplicity of modeling. Note: PAT supports two assignment syntax sugars ++, --. x++ is
same as x=x+1. y-- is same as y = y-1. y=x++
is same as x = x +1; y = x;. There is no support
for other shorthands, such as ++b , --b ,
b *= 2 , b += a , etc. Where needed,
their effect can be reproduced by using the non-shortened equivalents. The
following example shows the usage of ++ and --, where the final values of x and
y are both 3. var x = 2; var y; Invisible Events User can explicitly write invisible event (i.e., tau event) by using keyword
tau, e.g., tau -> Stop. In the tau event,
statement block can still be attached. With the support of tau
event, you can avoid using hiding operator to explicitly hide some visible
events by name them tau events. The second way to write an invisible event is to
skip the event name of a statement block, e.g., {x=x+1;} -> Stop, which is
equivalent to tau{x=x+1;} -> Stop. Processes may communicate through channels. Channel input/output is written
in a similar way as simple event prefixing. Let P be a process
expression. c!a.b
->
P
-- channel output c?x.y
->
P
-- channel input c?1 ->
P
-- channel input with expected value c?[x+y+9>10]x.y->
P -- channel input with guard
expression Where c is a channel, a and
b are expressions which evaluates to values (at run
time), while x and y are (local) variables which
take the input values. A channel must be declared before it is used. For channel
output, the compound value evaluated from both a and
b is stored in the channel buffer (FIFO queue) if the buffer
is not full yet. If the buffer is full, the process waits. For channel input
c?x.y, the top
element on the buffer is retrieved and then assigned to local
free variables x and y if the buffer is not empty.
Otherwise, it waits. For channel input c?1, the top element on the buffer is
retrieved if the buffer is not empty and the top element value is 1.
Otherwise, it waits. For channel input c?[x+y+9>10]x.y, the top element on
the buffer is retrieved and then assigned to local free variable x
and y if the buffer is not empty, and the
guard condition x+y+9>10 is true. Otherwise, it
waits. Note that in channel input, you can write expressions after c?, but
the expressions can not contain any global variables. You can put arbitrary
number of variables/expressions in the channel output/input by separating
them using '.'. The following example demonstrates how
channel communication is used. channel c 1; Sender(i) = c!i -> Sender(i); System() = Sender(5) ||| Receiver(); PAT supports synchronous channel communication, i.e., the channel output
and its matching channel input are engaged together. The synchronous
channel event will be displayed as c.exp for channel
output c!exp and channel input c?x. To do
synchronous channel communication, simply set the size of the channel to be
0. All the channel communications for non-zero channel are asynchronous. Channel communication can also attach program for both synchronous
and asynchronous channel. channel c 0; //or channel c 1;
P = c!x{ x = 2 } -> P; For the example above, the execution sequence is c!x -> (x = 2) ->
c?y -> (x = y). Note: Channel input variables' scope is after the channel
input event and within residing process. They can be referenced in the
scope, but not updated. Note: Parameter variables can be used in the expressions of
channel input, e.g., P(i) = c?i.i+1 -> Skip. In this case, once
the value of parameter i is known, i and i+1 will be
instantiated to constants, so that only matching channel output data will
be received. Furthermore, local free variable in channel input can also be
used in follow-up channel input's expressions. e.g., P() = c!5
-> c?x -> c!6 -> c?x+1 -> Skip; In this case, x
is 5 and P can execute to Skip. Global variables CAN NOT be used in
channel input expressions! PAT also support channel arrays, which is a syntax suger to make the modeling
easier if the channels are parameterized. The following syntax demonstrates
how to use the channel array. channel c[3] 1; Sender(i) = c[i]!i -> Sender(i); System() = (||| i:{0..2}@Sender(i) ) ||| Receiver(); Note: Two or N dimentional channel array can be simulated by
using 1 dimentional channel array. Hence, we don't provide syntax support for
that. For example channel c[3][5] 1 is same as channel c[15]
1, and c[2][3]!4 -> Skip is same as c[2*N+3]!4 ->
Skip, where N is the first dimention. Channel operations PAT provides 5 channel operations to query the buffer information of
asynchronous channels: cfull, cempty, ccount, csize, cpeek. The usage of these operations follows the
normal static method call, i.e., call(channel_operation, channel_name). The meaning of each
operation is explained below. Note: Parsing error message will be poped up if these
operations are applied to a synchronous channel. Note: Run time exception will be thrown if trying to
cpeek an empty buffer. A sequential composition is written as, P; Q where P and Q are processes. In this
process, P starts first and Q starts only when P has finished. General/External/Internal choice In PAT (as in CSP), we distinguish among general choice, external
choice and internal choice. General choice is resolved by any
event. A general choice is written as follows, P [] Q The choice operator [] states that either P or Q may
execute. If P performs an event first, then P takes control.
Otherwise, Q takes control. Notice that the semantic is a bit
different from the external choice below. External choice is resolved by the environment, e.g., the observation of
a visible event (i.e., not tau event). Notice that if
the first event of both P and Q is visible, then P[]Q and P[*]Q
are equivalent. An external choice is written as follows, P [*] Q The choice operator [*] states that either P or Q may
execute. If P performs a visible event first, then P takes
control. If Q performs a visible event first, then Q takes
control. Otherwise, the choice remains. Internal choice introduces non-determinism explicitly. The following models
an internal choice, P <> Q where either P or Q may execute. The
choice is made internally and non-deterministically. Non-determinism is largely
undesirable at design or implementation stage, whereas it is useful at modeling
stage for hiding irrelevant information. For instance, it can be used to model
the behaviors of a black-box procedure, where the exact details of the implementation are not available. The generalized form of general/external/internal choice is written as, [] x:{1..n}@
P(x)
-- which is equivalent to P(1) [] ... [] P(n) [*] x:{1..n}@
P(x)
-- which is equivalent to P(1) [*] ... [*] P(n) <> x:{1..n}@
P(x)
-- which is equivalent to P(1) <> ... <>
P(n) A choice may depend on a Boolean expression which in turn depends on the
valuations of the variables. In PAT, we support the classic if-then-else as
follows, if (cond) { P } else { Q } if (cond1) { P } else if (cond2) { Q } else
{ M } where cond is a
Boolean formula. If cond evaluates to true, the
P executes, otherwise Q executes. Notice that the else-part is
optional. The process if(false) {P}
behaves exactly as process Skip. PAT also provides atomic conditional choices, which perform
the condition checking and first operation of P/Q together.
This allows users to simulate CAS operator in distributed systems. The
syntax is following: ifa (cond) { P } else { Q
} PAT provides blocking conditional choices, which are similar to guarded process. The
only difference is that the checking of blocking condition and the execution of
P are separated in ifb. The syntax is
following. Note that there is no else in
ifb. ifb (cond) { P } Note: Side effect (i.e., update of the variable
value) is not allowed in if condition (similarly for guarded
process and case process below). This restriction is mainly for using
C# code in if condition. For example, a Boolean method isEmpty of a
user defined list variable returns a false and also adds an element to the list.
We add this restriction is purely for performance reason. If you really want to
achieve this effect, you can put the method call in an event prefix,
and store the returned value in a global Boolean variable. The global
variable can then be used in the if condition then. A generalized form of conditional choice is written as, where case is a key word and
cond1, cond2 are Boolean expressions. if
cond1 is true, then P1 executes. Otherwise, if
cond2 is true, then P2. And if cond1 and
cond2 are both false, then P executes by default. The condition is
evaluated one by one until a true one is found. In case no condition is true,
the default process will be executed. A guarded process only executes when its guard condition is satisfied. In
PAT, a guard process is written as follows, [cond]
P where cond is a
Boolean formula and P is a process. If cond is true, P executes. Notice that
different from conditional choice, if cond is
false, the whole process will wait until cond
is true and then P executes. Two processes which run concurrently without barrier synchronization written
as, P ||| Q where ||| denotes interleaving. Both P and
Q may perform their local actions without synchronizing with each
other except termination events. If
one process generates termination event, this termination event cannot executed
directly unless all processes are emitting a termination event. For example the
following process will deadlock due to this constraint. Skip ||| Stop Notice that P and Q can still communicate via shared variables
or channels. The generalized form of interleaving is written as, ||| x:{0..n} @ P(x) PAT supports grouped interleaving processes or even infinite number of
processes running interleavingly, similarly, for parallel composition
and internal/external choices. All the syntaxes below are valid. ||| {50} @ P(); //50 P() running interleavingly. || {..} @ Q(); //infinite number of Q() running in
parallel. [] x:{0..2} @ (
(||| {x} @ P) ||| (||| {x} @ Q()); // this is
equivalent to (Skip|||Skip)[]((||| {1} @P()) ||| (||| {1} @Q()) ) []
((||| {2} @P()) |||(||| {2} @Q())); Note: ||| {0} @ P() is same as Skip. Note: Looping variables can also be used in the process
inside as process parameter. For example, the following definitions
are all valid in PAT. ||| x:{0..3} @ (a.x -> Skip) Note: in grouped processes, e.g., []x:{0..n}@P
or ||| {0} @ P() , n can be a global
constant or process parameter, but not a global variable. We make this
restriction for the performance reason. For example, the following definitions
are all valid in PAT. #define n 10;
|||x:{0..n}@P; Parallel composition of two processes with barrier synchronization is written
as, P || Q where || denotes parallel composition. Different
from interleaving, P and Q may perform lock-step synchronization,
i.e., P and Q simultaneously perform an event. For instance, if
P is a -> c -> Stop and Q is c -> Stop,
because c is both in the alphabet of P and Q, it becomes a
synchronization barrier. Therefore, at the beginning, only a can be engaged.
After that, c is engaged by P and
Q at the exactly same time. In general, all events which are in both
P and Q's alphabets must be synchronized. Notice that, which
events are synchronization barriers depends on the alphabets of P and
Q. In order to know what are the enabled
actions, we therefore must first calculate the alphabets. In tools like FDR, the shared alphabet of a parallel composition must be
explicitly given. In PAT, however, we have a procedure to automatically
calculate alphabets. The alphabet of a process is the set of events that the
process takes part in. For instance, given the process defined as follows, VM() = insertcoin -> coffee -> VM(); The alphabet of VM() is exactly the
set of events which constitute the process expression, i.e., {insertcoin, coffee}. However, calculating the alphabet
of a process is not always trivial. It may be complicated by two things. One is
process referencing. The other is process parameters. In the above example, the
process reference VM() happens to be the
same as the process whose alphabet is being calculated. Thus, it is not
necessarily to unfold VM() again. Should
a different process is referenced, we must unfold that
process and get its alphabet. For instance, assume VM() is now defined as follows, VM() = insertcoin -> Inserted(); To calculate the alphabet of VM(), we
must unfold process Inserted() and combine alphabets of Inserted()
with {insertcoin}. Notice that a simple
procedure must be used to prevent unfolding the same process again. However,
even with such a procedure, it may still be infeasible to calculate mechanically
the alphabet of a process. The complexity is due to process parameters. For
instance, given the following process, P(i) =
a.i -> P(i+1); Naturally, the unfolding is non-terminating. In general, there is no way to
solve this problem. Therefore, PAT offers two compromising ways to get the
alphabets. One is to use a reasonably simple procedure to calculate a default
alphabet of a process. When the default alphabet is not as expected, an advanced
user is allowed to define the alphabet of a process manually. We detail
the former in the following. First of all, alphabet of processes are calculated only when it is
necessary, which means, only when a parallel composition is evaluated. This
saves a lot of computational overhead. Processes in a large number of models
only communicate through shared variables. If no parallel composition is
present, there is no need to evaluate alphabets. We remark that when there is no
shared abstract events, process P ||| Q and P || Q
are exactly the same. Therefore, we recommend ||| when appropriate. When a
parallel composition is evaluated for the first time, the default alphabet of
each sub-process is calculated (if not manually defined). The procedure for
calculating the default alphabet works by retrieving all event constituting the
process expression and unfolding every newly-met process reference. It throws an
exception if a process reference is met twice with different parameters (which
probably indicates the unfolding is non-terminating). In such a case, PAT
expects the user to specify the alphabet of a process using the following
syntax, #alphabet P {...}; where P is process name and {...}
is the set of events which is
considered its alphabet. Notice that the event expressions may contain
variables. The rules is that if process P(X) is defined, you may have
alphabet definitions as follows, #alphabet P {a.X}; Once the alphabets of P and Q are identified, we calculate
their intersection. If P is ready to perform an event which is not in the
intersection, it may simply proceed, so does Q. If P is ready
to perform an event in the intersection, it has to wait until Q is also
ready to perform this event and then proceed together. Remarks: Data operations (i.e. the
events attached with programs) are not counted in the calculation of alphabets
to avoid data race on updating same global variables. The detailed explanation
and examples are available here (Question 3).
};
} -> P();
P()
= add{x++;} -> minus{x--;} -> event{y=x++;} -> Skip;
Receiver() = c?x -> a.x -> Receiver();
var x =
1;
Q = c?y{ x =
y; } -> Q;
A = P ||| Q;
Receiver() = c[0]?x -> a.x -> Receiver() [] c[1]?x -> a.x ->
Receiver() [] c[2]?x -> a.x -> Receiver();
|| x:{0..3} @ (a.x -> Skip \
{a.x})
[] x:{0..3} @ (ch!x
-> Skip)
P(n) =
|||x:{0..n}@Q;
Inserted() = coffee -> VM();
Q1() = P();
#alphabet Q1 {x};
Q2() = P();
#alphabet Q2 {y};
The philosophy is that we see both the process expression and alphabet as
signatures of a process (i.e., processes with the same process expression but
different alphabets are essentially different processes!).
The generalized parallel composition is written as,
|| x:{0..n} @ P(x);
The alphabet of each P(x) is calculated. An event can be engaged if and only if all processes whose alphabet contains this event are ready to perform it.
Remarks: The syntax sugar indexed event list can be
used in the definition of alphabets. For example:
#define N 2;
P = e.0.0 -> e.0.1 -> e.0.2 -> turns -> e.1.0 -> e.1.1 -> e.1.2 -> e.2.0 -> e.2.1 -> e.2.2 -> P;
#alphabet P { x:{0..N}; y:{0..N} @ e.x.y };
The above definitions define the alphabet of process P as
the set of all events except event turns appearing in its proces
definition.
Process P interrupt Q behaves as
specified by P until the first visible event of Q is engaged which
could be at any execution point of process P, and then the control
transfers to Q. An execution trace of process P interrupt Q is just a trace of P up to an
arbitrary point when the interrupt occurs, followed by any trace of
Q.
The following is an example,
- Err() = exception -> Err();
- Routine() = routine -> Routine();
- ExceptionHandling() = Routine() interrupt exception -> ExceptionHandling() ;
- System = Err() || ExceptionHandling();
where Routine() is a process which performs normal daily task,
Err() is a process modeling errors happened in the environment and ExceptionHandling() is a process which performs
necessary actions for error handling. For System, whenever an exception occurs
(modeled as event exception), process ExceptionHandling() takes the control
over.
Note: For process P interrupt Q, the interrupting event from Q must be a visible event (not tau). If a tau event is detected, a runtime exception will be thrown.
Process P \ A where A is a set of events turns events in A to invisible ones. Hiding is applied when only certain events are interested. Hiding may be used to introduce non-determinism. The following is an example,
dashPhil() = Phil() \ {getfork.1, getfork.2, putfork.1, putfork.2};
Phil() = getfork.1 -> getfork.2 -> eat -> putfork.1 -> putfork.2 -> Phil();
where process Phil() specifies a philosopher who gets two forks in order and then eats and then puts down both forks in the same order. Process dashPhil(), however, hides the events of getting up or putting down the forks. We can imagine that the philosopher is so quick that no one can tell how he gets the forks. People can only tell when he is eating. By hiding those events, the rest of the system can not observe those hidden events. We remark that hiding is often used to prevent unwanted synchronization in parallel composition.
Note: The syntax sugar indexed event list can be used for defining a set of events with the same prefix. For example, the definition for process dashPhil() can be rewritten as the following.
dashPhil() = Phil() \ { x:{1..2} @ getfork.x, y:{1..2} @ putfork.y} ;
The keyword atomic allows user to associate higher priority with a process, i.e., if the process has an enabled event, the event will execute before any events from non-atomic processes. The syntax is atomic{P}, where P is any process definition.
If a sequence of statements is enclosed in parentheses and prefixed with the keyword atomic, this indicates that the sequence is to be executed as one super-step, not to be interleaved by other processes. In the interleaving of process executions, no other process can execute statements from the moment that an event in an atomic process is enabled until the last enabled one has completed. The sequence can contain arbitrary process statements, and may be non-deterministic. Once an atomic process is enabled, it immeidately gains a higher priority. It continues to execute until it is disabled. Once all atomic processes are enabled, other non-atomic processes are then allowed to execute. If multiple atomic processes are enabled, then they interleave each other. In the following example, process P and Q will interleave each other, whereas W will excute only after event c and f have occurred.
channel ch 0;
P = atomic { a -> ch!0 -> b -> c -> Skip};
Q = atomic { d -> ch?0 -> e -> f -> Skip};W = g -> Skip
Sys = P ||| Q ||| W;
Note: Since PAT 3.4.2, the semantics of atomic process changed a little bit. In the example below, before PAT 3.4.2, event a and d are enabled at the same time when process Sys starts. In PAT 3.4.2, only d is enabled because enabled atomic process has higher priority than enabled events. This change allows us to use atomic consistently in CSP module and RTS module.
P = a -> atomic { b
-> c -> Skip};
Q = atomic { d -> e -> f ->
Skip};
Sys = P ||| Q;
Note: atomic sequences can be used for state reduction for model checking, especially if the process is composed with other processes in parallel. The number of states may be reduced exponentially. In a way, by using atomic, we may partial order reduction manually (without computational overhead). The general rule is that local events which are invisible to the verifying property and independent to other events shall be associated with higher priority.
Note: an atomic process inside other atomic process has no effect at all.
Recursion is achieved through process referencing flexibly. The following process contains mutual recursion.
P(i) = a.i -> Q(i);
Q(i) = b.i -> P(i);
System() = P(1) || Q(2);
Note: when invoking a process, the parameters can be any valid expression, e.g. P(x), P(x+1), P(new List()). Only when the process parameter is used as user defined types, it is user's responsibility to make sure that the correct variable type is passed in since most of PAT modules don't have explicit types. See the example below.
#import "PAT.Lib.Set";
var<Set>
set1;
Q() =
P(set1);
P(i)
= initialize{i.Add(1);}-> ([i.GetSize() > 0] Skip);
Warning: when user defined data structure is used as parameter, if the parameter in the process updates the data structure, the verification/simulation maybe wrong and un-expected. For instance the following example, i is an object used in both branch of the choice operator, so the effect of executing add1 will stay even the actual branch selected is add2. In the simulator, you will find that after executing event add2, the value of set1 can become [1,2]. The root of this cause is the pointer problem.
#import "PAT.Lib.Set";
var<Set>
set1;
Q() =
P(set1);
P(i) = add1{i.Add(1);} -> Skip [] add2{i.Add(2);} -> Skip;
It is straightforward to use process reference to realize common iterative procedures. For instance, the following process behaves exactly as while (cond) {P()};
Q() = if (cond) {P(); Q()};
Assertion process allows user to add an assertion in the program. PAT simulator and verifiers will check the assertion at run time. If the assertion is failed, a PAT runtime exception will be thrown to the user and the evaluation is stoped. The syntax of Assertion is as follows,
var x = 1;
P = assert(x > 0); e{x = x-1;} -> P;
Copyright © 2007-2012 Semantic Engineering Pte. Ltd.